Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		msort(nil)	→ nil
2:		msort(x . y)	→ min(x,y) . msort(del(min(x,y),x . y))
3:		min(x,nil)	→ x
4:		min(x,y . z)	→ if(x ≤ y,min(x,z),min(y,z))
5:		del(x,nil)	→ nil
6:		del(x,y . z)	→ if(x = y,z,y . del(x,z))

There are 6 dependency pairs:


7:		MSORT(x . y)	→ MSORT(del(min(x,y),x . y))
8:		MSORT(x . y)	→ DEL(min(x,y),x . y)
9:		MSORT(x . y)	→ MIN(x,y)
10:		MIN(x,y . z)	→ MIN(x,z)
11:		MIN(x,y . z)	→ MIN(y,z)
12:		DEL(x,y . z)	→ DEL(x,z)

The approximated dependency graph contains 3 SCCs: {12}, {10,11} and {7}.

Consider the SCC {12}. There are no usable rules. By taking the AF π with π(DEL) = 2 and π(.) = [2] together with the lexicographic path order with empty precedence, rule 12 is strictly decreasing.

Consider the SCC {10,11}. There are no usable rules. By taking the AF π with π(MIN) = 2 and π(.) = [2] together with the lexicographic path order with empty precedence, the rules in {10,11} are strictly decreasing.

Consider the SCC {7}. The usable rules are {3-6}. By taking the AF π with π(≤) = π(if) = π(min) = π(MSORT) = 1 and π(.) = π(=) = π(del) = [ ] together with the lexicographic path order with precedence . ≻ del ≻ = and del ≻ nil, the rules in {3,4} are weakly decreasing and the rules in {5-7} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.74 seconds) --- May 3, 2006